Nuprl Lemma : l_contains_weakening
0,22
postcript
pdf
T
:Type,
A
,
B
:
T
List.
A
=
B
l_contains(
T
;
A
;
B
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
P
Q
,
x
L
.
P
(
x
)
,
l_contains(
T
;
A
;
B
)
,
Prop
Lemmas
l
contains
wf
,
l
member
wf
origin
T:Type, A, B:T List. A = B 
l_contains(T;A;B) T:Type, A, B:T List. A = B l_contains(T;A;B) 
Tx:A. B(x) l) QxL. P(x)